A,B:es_realizer{i:l}. R-frame-compat(A; B)  prop{i:l} 

latex

Definitions

x. t(x), ff, tt, P  Q, if b then t else f fi , R-frame-compat(A; B), prop{i:l}, t  T, x:A. B(x), x(s), P  Q, P  Q, Unit, ,

Lemmas

es realizer wf, Rpre-a wf, locl wf, Rpre-ds wf, Rpre? wf, Rbframe-L wf, Rbframe-k wf, Rbframe? wf, Rsframe-L wf, Rsends-knd wf, Rsends-g wf, pi1 wf, Rsends-dt wf, decl-type wf, Rsends-T wf, Rsends-ds wf, decl-state wf, map wf, Rsframe-tag wf, Rsends-l wf, Rsframe-lnk wf, IdLnk wf, Rsframe? wf, Rsends? wf, true wf, Rrframe-L wf, Rrframe-x wf, top wf, fpf wf, fpf-trivial-subtype-top, Reffect-ds wf, id-deq wf, fpf-dom wf, Rrframe? wf, Raframe-L wf, Raframe-k wf, Raframe? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rframe-L wf, Reffect-knd wf, Knd wf, l member wf, Reffect-x wf, Rframe-x wf, Id wf, Rframe? wf, eqtt to assert, bool wf, Reffect? wf